YES 3.329 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



Lambda Reductions:
The following Lambda expression
\_→q

is transformed to
gtGt0 q _ = q



↳ HASKELL
  ↳ LR
HASKELL
      ↳ IFR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



If Reductions:
The following If expression
if b then (showChar '(') . p . showChar ')' else p

is transformed to
showParen0 p True = (showChar '(') . p . showChar ')'
showParen0 p False = p



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
HASKELL
          ↳ BR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
HASKELL
              ↳ COR

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
HASKELL
                  ↳ NumRed

mainModule Main
  ((print :: Ordering  ->  IO ()) :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ IFR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ NumRed
HASKELL
                      ↳ Narrow

mainModule Main
  (print :: Ordering  ->  IO ())

module Main where
  import qualified Prelude



Haskell To QDPs